<html>
<head><meta charset="utf-8"><title>Will polonius help with cases like this? · t-compiler/wg-polonius · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/index.html">t-compiler/wg-polonius</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html">Will polonius help with cases like this?</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="223807782"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223807782" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> panstromek <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223807782">(Jan 24 2021 at 10:46)</a>:</h4>
<p>This code doesn't compile, but arguably it should (at least in my opinion). I wonder if this is the case where Polonius relaxes the analysis, because this specific case is annoying me a lot pretty often. </p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">struct</span> <span class="nc">Point</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">x</span>:<span class="kt">i32</span><span class="p">,</span><span class="w"> </span><span class="n">y</span>:<span class="kt">i32</span> <span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">accept</span><span class="p">(</span><span class="n">point</span>: <span class="kp">&amp;</span><span class="nc">mut</span><span class="w"> </span><span class="n">Point</span><span class="p">)</span><span class="w"> </span><span class="p">{}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">main</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="kd">let</span><span class="w"> </span><span class="k">mut</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">Point</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">x</span>:<span class="mi">0</span><span class="p">,</span><span class="w"> </span><span class="n">y</span>:<span class="mi">0</span><span class="w"> </span><span class="p">};</span><span class="w"></span>
<span class="w">    </span><span class="kd">let</span><span class="w"> </span><span class="k">mut</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="k">mut</span><span class="w"> </span><span class="n">p</span><span class="p">.</span><span class="n">x</span><span class="p">;</span><span class="w"></span>
<span class="w">    </span><span class="c1">// *x = 3; // it should be ok even if you uncomment this line</span>
<span class="w">    </span><span class="n">accept</span><span class="p">(</span><span class="o">&amp;</span><span class="k">mut</span><span class="w"> </span><span class="n">p</span><span class="p">);</span><span class="w"></span>
<span class="w">    </span><span class="c1">// let mut x = &amp;mut p.x;  //rebinding here fixes the problem</span>
<span class="w">    </span><span class="o">*</span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">3</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>
<p>Interestingly, there's a lot of very similar cases that shouldn't compile, which probably makes this challenging. <del>Even just adding one level of nesting breaks this.</del> Maybe not, actually, I'll have to think about it more</p>



<a name="223811067"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223811067" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223811067">(Jan 24 2021 at 12:12)</a>:</h4>
<p>If you make <code>accept</code> actually mutate the <code>point</code>, your code has UB under Stacked Borrows (and most aliasing models I can imagine). Which is to say, the code is wrong and should not be accepted by the compiler.</p>



<a name="223811082"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223811082" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223811082">(Jan 24 2021 at 12:13)</a>:</h4>
<p>One key promise for mutable references like <code>x</code> is that if you use them twice, and there was no other use or reborrow of <code>x</code> in between, then the pointee is unchanged. So in code like</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="o">*</span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">3</span><span class="p">;</span><span class="w"></span>
<span class="n">accept</span><span class="p">(</span><span class="o">&amp;</span><span class="k">mut</span><span class="w"> </span><span class="n">p</span><span class="p">);</span><span class="w"></span>
<span class="o">*</span><span class="n">x</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="mi">3</span><span class="p">;</span><span class="w"></span>
</code></pre></div>
<p>it is very important that <code>accept</code> cannot mutate what <code>x</code> points to.</p>



<a name="223811084"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223811084" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223811084">(Jan 24 2021 at 12:13)</a>:</h4>
<p>If your code was accepted, it could violate this property, which would be bad.</p>



<a name="223811143"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223811143" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223811143">(Jan 24 2021 at 12:14)</a>:</h4>
<p>(in fact, it is easy to change this example such that if very similar code was accepted we'd have use-after-free... just make <code>p</code> a <code>Vec</code> and <code>x = &amp;mut p[0]</code>)</p>



<a name="223812527"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223812527" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> panstromek <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223812527">(Jan 24 2021 at 12:52)</a>:</h4>
<p>The key here is that when <code>accept</code> mutates the point, the reference in <code>x</code> is not "active" and accept cannot possibly change its value - because it is just a static offset. Rebinding it afterwards is just a no-op, which seems to me like the compiler should be able to reason about automatically -  and it already does to some extent, because it "deactivates" the reference before calling accept. It could "just" (with a lot of caveats) reactivate it afterwards.</p>
<p>The example with a Vec is what is exactly what I had in mind with similar cases that shouldn't compile, but my example only cares about structs, ie. things that are known at compile time.</p>
<p>It's sort of a multi-phase borrow or something like that.</p>



<a name="223812594"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223812594" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> panstromek <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223812594">(Jan 24 2021 at 12:54)</a>:</h4>
<p>I'd summarize this as - if some borrow checker error can be fixed by <code>let</code> rebinding that is provably no-op, it shouldn't be a borrow checker error in the first place.</p>



<a name="223814537"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223814537" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223814537">(Jan 24 2021 at 13:41)</a>:</h4>
<p>Every time you make a new borrow you are asserting that you can read/write (depending on if the borrow is mutable) the pointed to memory, so borrowing isn't a no-op.</p>



<a name="223815780"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223815780" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> panstromek <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223815780">(Jan 24 2021 at 14:11)</a>:</h4>
<p>I still don't understand why would that be a problem. This is code can easily be fixed by just re-binding <code>x</code> without any change in behaviour. Why couldn't this transformation be done automatically, when possible?</p>



<a name="223816411"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223816411" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223816411">(Jan 24 2021 at 14:27)</a>:</h4>
<p>Because it changes behavior. It invalidates other borrows. Drops are also not moved earlier when doing so would be necessary to fix a borrowck error. This no surprises behavior is essential when writing unsafe code.</p>



<a name="223817047"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223817047" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> panstromek <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223817047">(Jan 24 2021 at 14:43)</a>:</h4>
<p>Drop is still observable behaviour, though. Borrow is just a semantic construct. I can't imagine a case where this could break something, if implemented. Can you give an example where this would cause a problem?</p>



<a name="223826817"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223826817" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223826817">(Jan 24 2021 at 18:10)</a>:</h4>
<blockquote>
<p>The key here is that when accept mutates the point, the reference in x is not "active" and accept cannot possibly change its value</p>
</blockquote>
<p>It <em>is</em> active though. Any reference that will be used again is "active".<br>
Not sure what notion of "active" you are talking about, but it does not seem to be the one used in Rust.</p>



<a name="223826909"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Will%20polonius%20help%20with%20cases%20like%20this%3F/near/223826909" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Will.20polonius.20help.20with.20cases.20like.20this.3F.html#223826909">(Jan 24 2021 at 18:12)</a>:</h4>
<p>Also note that borrow checking is deliberately designed to work the same for all kinds of types -- your example is clearly wrong with <code>Vec</code>, so not accepting it for <code>Pair</code> is by-design. This has several advantages:</p>
<ul>
<li>It means the rules are simpler, and as such easier to design, implement, explain, and understand.</li>
<li>It means the rules are more universal, which can be exploited for some really nifty optimizations.</li>
</ul>
<p>It has the disadvantage that there is some code that does not trigger use-after-free that is rejected by the compiler, such as your example. This price IMO is worth paying for the above benefits.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>